We will now introduce an induction principle for lists. It is derived directly from the definition of the list datatype.
Induction Principle (Lists)
P [] P (t) => P (h :: t)
Proposition (Interchange)
The rev function and the append operator obey an interchange law since the following holds for all 'a lists l1 and l2.
rev (l1 @ l2) = rev l2 @ rev l1
Exercise
Prove by structural induction that for all 'a lists l1 and l2:length (l1 @ l2) = length l1 + length l2
Proposition (Involution)
The rev function is an involution, i.e. it always undoes its own work, since rev (rev l) = l.